package trabajoISW2.domain.contracts;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;

@Inv({"getAddressId() >= 0 && getAddressId() <= Integer.MAX_VALUE" })
public interface IAddress {
	
	@Pre({"id >= 0 #WrongIdException", "id <= Integer.MAX_VALUE #WrongIdException"})
	@Pos("getAddressId() == id")
	public void setAddressId(int id);
	
	
	@Query
	public int getAddressId();
	
	@Pre({"address.compareTo(\"\") != 0 #WrongNameException", "address != null #WrongNameException"})
	@Pos("getAddress().compareTo(address) == 0")
	public void setAddress(String address);
	
	@Query
	public String getAddress();
	
	@Pre("zc > 0 && zc < Integer.MAX_VALUE  #NoPositiveNumberException")
	@Pos({"getZipCode().compareTo(zc)"})
	public void setZipCode(int zc);
	
	@Query
	public int getZipCode();
	
	@Pre({"city.compareTo.(\"\") != 0 #WrongNameException", "city!=null #WrongNameException"})
	@Pos({"getCity().compareTo(city) == 0"})
	public void setCity(String city);
	
	@Query
	public String getCity();
	
	@Pre({"country.compareTo(\"\") != 0 #WrongNameException", "country != null #WrongNameException"})
	@Pos("getCountry().compareTo(country) == 0")
	public void setCountry(String country);
	
	@Query
	public String getCountry();

}
